KILLED



    


Runtime Complexity (full) proof of /tmp/tmpiy6gUH/t009.xml









The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

0 CpxTRS


↳1 DecreasingLoopProof (⇔, 8332 ms)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)

busy(BF, d, stop, b1, b2, b3, i) → incorrect

busy(FS, d, stop, b1, b2, b3, i) → incorrect

busy(fl, open, up, b1, b2, b3, i) → incorrect

busy(fl, open, down, b1, b2, b3, i) → incorrect

busy(B, closed, stop, false, false, false, empty) → correct

busy(F, closed, stop, false, false, false, empty) → correct

busy(S, closed, stop, false, false, false, empty) → correct

busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))

busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))

busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))

busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)

busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)

busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)

busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)

busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)

busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)

busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)

busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)

busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)

busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)

busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)

busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)

busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)

busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)

busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)

busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)

busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)

busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)

busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)

busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)

busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)

busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)

busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)

busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)

busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)

idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

or(true, b) → true

or(false, b) → b

Rewrite Strategy: FULL




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
idle(B, d, stop, false, b2, b3, newbuttons(true, i2, i3, i)) →+ idle(B, open, stop, false, or(b2, i2), or(b3, i3), i)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [i / newbuttons(true, i2, i3, i)].
The result substitution is [d / open, b2 / or(b2, i2), b3 / or(b3, i3)].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)

busy(BF, d, stop, b1, b2, b3, i) → incorrect

busy(FS, d, stop, b1, b2, b3, i) → incorrect

busy(fl, open, up, b1, b2, b3, i) → incorrect

busy(fl, open, down, b1, b2, b3, i) → incorrect

busy(B, closed, stop, false, false, false, empty) → correct

busy(F, closed, stop, false, false, false, empty) → correct

busy(S, closed, stop, false, false, false, empty) → correct

busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))

busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))

busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))

busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)

busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)

busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)

busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)

busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)

busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)

busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)

busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)

busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)

busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)

busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)

busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)

busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)

busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)

busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)

busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)

busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)

busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)

busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)

busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)

busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)

busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)

busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)

busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)

busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)

idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

or(true, b) → true

or(false, b) → b

S is empty.
Rewrite Strategy: FULL




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
TRS:
Rules:
start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Types:
start :: empty:newbuttons → incorrect:correct
busy :: F:BF:FS:B:S → closed:open → stop:up:down → false:true → false:true → false:true → empty:newbuttons → incorrect:correct
F :: F:BF:FS:B:S
closed :: closed:open
stop :: stop:up:down
false :: false:true
BF :: F:BF:FS:B:S
incorrect :: incorrect:correct
FS :: F:BF:FS:B:S
open :: closed:open
up :: stop:up:down
down :: stop:up:down
B :: F:BF:FS:B:S
empty :: empty:newbuttons
correct :: incorrect:correct
S :: F:BF:FS:B:S
newbuttons :: false:true → false:true → false:true → empty:newbuttons → empty:newbuttons
idle :: F:BF:FS:B:S → closed:open → stop:up:down → false:true → false:true → false:true → empty:newbuttons → incorrect:correct
true :: false:true
or :: false:true → false:true → false:true
hole_incorrect:correct1_0 :: incorrect:correct
hole_empty:newbuttons2_0 :: empty:newbuttons
hole_F:BF:FS:B:S3_0 :: F:BF:FS:B:S
hole_closed:open4_0 :: closed:open
hole_stop:up:down5_0 :: stop:up:down
hole_false:true6_0 :: false:true
gen_empty:newbuttons7_0 :: Nat → empty:newbuttons




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
busy, idle
They will be analysed ascendingly in the following order:
busy = idle




(8) Obligation:
TRS:
Rules:
start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Types:
start :: empty:newbuttons → incorrect:correct
busy :: F:BF:FS:B:S → closed:open → stop:up:down → false:true → false:true → false:true → empty:newbuttons → incorrect:correct
F :: F:BF:FS:B:S
closed :: closed:open
stop :: stop:up:down
false :: false:true
BF :: F:BF:FS:B:S
incorrect :: incorrect:correct
FS :: F:BF:FS:B:S
open :: closed:open
up :: stop:up:down
down :: stop:up:down
B :: F:BF:FS:B:S
empty :: empty:newbuttons
correct :: incorrect:correct
S :: F:BF:FS:B:S
newbuttons :: false:true → false:true → false:true → empty:newbuttons → empty:newbuttons
idle :: F:BF:FS:B:S → closed:open → stop:up:down → false:true → false:true → false:true → empty:newbuttons → incorrect:correct
true :: false:true
or :: false:true → false:true → false:true
hole_incorrect:correct1_0 :: incorrect:correct
hole_empty:newbuttons2_0 :: empty:newbuttons
hole_F:BF:FS:B:S3_0 :: F:BF:FS:B:S
hole_closed:open4_0 :: closed:open
hole_stop:up:down5_0 :: stop:up:down
hole_false:true6_0 :: false:true
gen_empty:newbuttons7_0 :: Nat → empty:newbuttons
Generator Equations:
gen_empty:newbuttons7_0(0) ⇔ empty
gen_empty:newbuttons7_0(+(x, 1)) ⇔ newbuttons(false, false, false, gen_empty:newbuttons7_0(x))
The following defined symbols remain to be analysed:
idle, busy
They will be analysed ascendingly in the following order:
busy = idle